/-
Copyright (c) 2025 Etienne Marion. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Etienne Marion
-/
module

public import Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd
public import Mathlib.Probability.Independence.Process
public import Mathlib.Probability.Notation

/-!
# Characterizing independence via bounded continuous functions

Given two random variables `X : Ω → E` and `Y : Ω → F` such that `E` and `F` are Borel spaces
satisfying `HasOuterApproxClosed`, `X` and `Y` are independent if for any real bounded continuous
functions `f` and `g`, `∫ ω, f (X ω) * g (Y ω) ∂P = (∫ ω, f (X ω) ∂P) * (∫ ω, g (Y ω) ∂P)`.

Consider now `X : (s : S) → Ω → E s`, with `Fintype S` and each `E s` being a Borel space satisfying
`HasOuterApproxClosed`. Then to apply the above result we need that `Π s, E s` is a Borel space,
and therefore that each `E s` is second countable. We can circumvent this restriction by proving
that `fun ω s ↦ X s ω` and `Y` are independent if for any family of bounded continuous functions
`f : (s : S) → E s → ℝ` and any bounded continuous function `g : F → ℝ` we have
`∫ ω, ∏ s, f s (X s ω) * g (Y ω) ∂P = ∫ ω, ∏ s, f s (X s ω) ∂P * ∫ ω, g (Y ω) ∂P`.
We can use this result in the case where `S := Unit` to deduce the first statement we mentioned.

We take this approach in this file. We first prove `pi_indepFun_pi_of_prod_bcf`, which allows to
prove the result when `E` and `F` are product spaces without assuming second countability, and
then we deduce the other cases from there.

Building on this, we also prove `process_indepFun_process_of_prod_bcf`. This time we do not require
`Fintype S` and require the hypothesis to be satisfied for each `I : Finset S`. Then we similarly
deduce other versions where one of the variables is not necessarily a process.

We then turn to independence between an event and a random variable. We prove
`indicator_indepFun_pi_of_prod_bcf`: the indicator of an event `A` is independent
of a finite family of random variables `X : (s : S) → Ω → E s` if for any family of bounded
continuous functions `f : (s : S) → E s → ℝ` we have
`∫ ω in A, ∏ s, f s (X s ω) ∂P = P.real A * ∫ ω, ∏ s, f s (X s ω) ∂P`. Once again we deduce
other versions from this, and also write versions where `X` is a stochastic process.

Then we build on that to show that a `σ`-algebra `m` is independent from a stochastic process `X`
if for any `A` such that `MeasurableSet[m] A`, any `I : Finset S` and any bounded continuous
function `f : (Π s : I, E s) → ℝ`, we have `∫ ω in A, f (X · ω) ∂P = P.real A * ∫ ω, f (X · ω) ∂P`.
This again is formulated with different versions. We also provide versions in terms of
`IndepSets` instead of `Indep`.

## Main statement

* `indep_comap_process_of_bcf`: A `σ`-algebra `m` is independent from a stochastic process `X`
  if for any `A` such that `MeasurableSet[m] A`, any `I : Finset S`, and any bounded continuous
  function `f : (Π s : I, E s) → ℝ`, we have
  `∫ ω in A, f (X · ω) ∂P = P.real A * ∫ ω, f (X · ω) ∂P`.

## Notations

to avoid writing `boundedContinuousFunction` in the names, which is quite lengthy, we abbreviate it
to `bcf`.

## Tags

independence, bounded continuous functions
-/

@[expose] public section

open MeasureTheory Measure ProbabilityTheory ENNReal
open scoped BoundedContinuousFunction

variable {Ω S T : Type*} {m mΩ : MeasurableSpace Ω} {P : Measure Ω}

/-- If the indicator of a set `A` is indepent from a variable `X`, then set `A` is independent
from the sigma algebra generated by `X`. -/
lemma IndepFun.singleton_indepSets_of_indicator {𝓧 : Type*} [mX : MeasurableSpace 𝓧] {A : Set Ω}
    {X : Ω → 𝓧} (h : (A.indicator (1 : Ω → ℝ)) ⟂ᵢ[P] X) :
    IndepSets {A} {s | MeasurableSet[mX.comap X] s} P := by
  rw [IndepSets_iff]
  rintro s - hs ⟨t, ht, rfl⟩
  rw [Set.mem_singleton_iff.1 hs]
  have hA' : A = A.indicator (1 : Ω → ℝ) ⁻¹' {1} := by ext; simp [Set.indicator]
  rw [hA']
  exact h.measure_inter_preimage_eq_mul _ _ (by simp) ht

variable {E : S → Type*} {F : T → Type*} {G H : Type*}
  [∀ s, TopologicalSpace (E s)] [∀ s, MeasurableSpace (E s)] [∀ s, BorelSpace (E s)]
  [∀ s, HasOuterApproxClosed (E s)]
  [∀ t, TopologicalSpace (F t)] [∀ t, MeasurableSpace (F t)] [∀ t, BorelSpace (F t)]
  [∀ t, HasOuterApproxClosed (F t)]
  [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G] [HasOuterApproxClosed G]
  [TopologicalSpace H] [MeasurableSpace H] [BorelSpace H] [HasOuterApproxClosed H]
  {X : (s : S) → Ω → E s} {Y : (t : T) → Ω → F t} {Z : Ω → G} {U : Ω → H}

section Fintype

variable [Fintype S] [Fintype T]

section IndepFun

variable [IsFiniteMeasure P]

lemma pi_indepFun_pi_of_prod_bcf (mX : ∀ s, AEMeasurable (X s) P)
    (mY : ∀ t, AEMeasurable (Y t) P)
    (h : ∀ (f : (s : S) → E s →ᵇ ℝ) (g : (t : T) → F t →ᵇ ℝ),
      P[(∏ s, f s ∘ (X s)) * (∏ t, g t ∘ (Y t))] = P[∏ s, f s ∘ (X s)] * P[∏ t, g t ∘ (Y t)]) :
    IndepFun (fun ω s ↦ X s ω) (fun ω t ↦ Y t ω) P := by
  rw [indepFun_iff_map_prod_eq_prod_map_map (aemeasurable_pi_lambda _ mX)
    (aemeasurable_pi_lambda _ mY)]
  refine eq_prod_of_integral_prod_mul_prod_boundedContinuousFunction fun f g ↦ ?_
  rw [integral_map, integral_map, integral_map]
  · convert h f g <;> simp
  any_goals fun_prop
  all_goals exact Measurable.aestronglyMeasurable (by fun_prop)

/-- Two families of random variables $(X_1, ..., X_p)$ and $(Y_1, ..., Y_q)$ are independent if
for all real bounded continuous functions $f$ and $g$,
$$P[f(X_1, ..., X_p) g(Y_1, ..., Y_q)] = P[f(X_1, ..., X_p)] * P[g(Y_1, ..., Y_q)].$$ -/
lemma pi_indepFun_pi_of_bcf (mX : ∀ s, AEMeasurable (X s) P)
    (mY : ∀ t, AEMeasurable (Y t) P)
    (h : ∀ (f : (Π s, E s) →ᵇ ℝ) (g : (Π t, F t) →ᵇ ℝ),
      P[fun ω ↦ f (X · ω) * g (Y · ω)] = P[fun ω ↦ f (X · ω)] * P[fun ω ↦ g (Y · ω)]) :
    IndepFun (fun ω s ↦ X s ω) (fun ω t ↦ Y t ω) P := by
  refine pi_indepFun_pi_of_prod_bcf mX mY fun f g ↦ ?_
  convert h (∏ s, (f s).compContinuous ⟨Function.eval s, by fun_prop⟩)
    (∏ t, (g t).compContinuous ⟨Function.eval t, by fun_prop⟩) <;> simp

lemma indepFun_pi_of_prod_bcf (mZ : AEMeasurable Z P)
    (mY : ∀ t, AEMeasurable (Y t) P)
    (h : ∀ (f : G →ᵇ ℝ) (g : (t : T) → F t →ᵇ ℝ),
      P[f ∘ Z * (∏ t, g t ∘ (Y t))] = P[f ∘ Z] * P[∏ t, g t ∘ (Y t)]) :
    IndepFun Z (fun ω t ↦ Y t ω) P := by
  rw [indepFun_iff_map_prod_eq_prod_map_map mZ (aemeasurable_pi_lambda _ mY)]
  refine eq_prod_of_integral_mul_prod_boundedContinuousFunction fun f g ↦ ?_
  rw [integral_map, integral_map, integral_map]
  · convert h f g <;> simp
  any_goals fun_prop
  all_goals exact Measurable.aestronglyMeasurable (by fun_prop)

lemma indepFun_pi_of_bcf (mZ : AEMeasurable Z P)
    (mY : ∀ t, AEMeasurable (Y t) P)
    (h : ∀ (f : G →ᵇ ℝ) (g : (Π t, F t) →ᵇ ℝ),
      P[fun ω ↦ f (Z ω) * g (Y · ω)] = P[f ∘ Z] * P[fun ω ↦ g (Y · ω)]) :
    IndepFun Z (fun ω t ↦ Y t ω) P := by
  refine indepFun_pi_of_prod_bcf mZ mY fun f g ↦ ?_
  convert h f (∏ t, (g t).compContinuous ⟨Function.eval t, by fun_prop⟩) <;> simp

lemma pi_indepFun_of_prod_bcf (mX : ∀ s, AEMeasurable (X s) P)
    (mU : AEMeasurable U P)
    (h : ∀ (f : (s : S) → E s →ᵇ ℝ) (g : H →ᵇ ℝ),
      P[(∏ s, f s ∘ (X s)) * g ∘ U] = P[∏ s, f s ∘ (X s)] * P[g ∘ U]) :
    IndepFun (fun ω s ↦ X s ω) U P := by
  rw [indepFun_iff_map_prod_eq_prod_map_map (aemeasurable_pi_lambda _ mX) mU]
  refine eq_prod_of_integral_prod_mul_boundedContinuousFunction fun f g ↦ ?_
  rw [integral_map, integral_map, integral_map]
  · convert h f g <;> simp
  any_goals fun_prop
  all_goals exact Measurable.aestronglyMeasurable (by fun_prop)

lemma pi_indepFun_of_bcf (mX : ∀ s, AEMeasurable (X s) P)
    (mU : AEMeasurable U P)
    (h : ∀ (f : (Π s, E s) →ᵇ ℝ) (g : H →ᵇ ℝ),
      P[fun ω ↦ f (X · ω) * g (U ω)] = P[fun ω ↦ f (X · ω)] * P[g ∘ U]) :
    IndepFun (fun ω s ↦ X s ω) U P := by
  refine pi_indepFun_of_prod_bcf mX mU fun f g ↦ ?_
  convert h (∏ s, (f s).compContinuous ⟨Function.eval s, by fun_prop⟩) g <;> simp

/-- Two random variables $X$ and $Y$ are independent if
for all real bounded continuous functions $f$ and $g$,
$$P[f(X) g(Y)] = P[f(X)] * P[g(Y)].$$ -/
lemma indepFun_of_bcf (mZ : AEMeasurable Z P) (mU : AEMeasurable U P)
    (h : ∀ (f : G →ᵇ ℝ) (g : H →ᵇ ℝ), P[f ∘ Z * g ∘ U] = P[f ∘ Z] * P[g ∘ U]) :
    IndepFun Z U P := by
  rw [indepFun_iff_map_prod_eq_prod_map_map mZ mU]
  refine eq_prod_of_integral_mul_boundedContinuousFunction fun f g ↦ ?_
  rw [integral_map, integral_map, integral_map]
  · exact h f g
  any_goals fun_prop
  exact Measurable.aestronglyMeasurable (by fun_prop)

end IndepFun

variable [IsProbabilityMeasure P]

section Indicator

lemma indicator_indepFun_pi_of_prod_bcf
    {A : Set Ω} (mA : NullMeasurableSet A P) (mX : ∀ s, AEMeasurable (X s) P)
    (h : ∀ f : (s : S) → E s →ᵇ ℝ, ∫ ω in A, ∏ s, f s (X s ω) ∂P =
      P.real A * ∫ ω, ∏ s, f s (X s ω) ∂P) :
    (A.indicator (1 : Ω → ℝ)) ⟂ᵢ[P] (fun ω s ↦ X s ω) := by
  refine indepFun_pi_of_prod_bcf
    ((aemeasurable_indicator_const_iff 1).2 mA) mX fun f g ↦ ?_
  have h1 ω : f (A.indicator 1 ω) * ∏ s, g s (X s ω) =
      A.indicator (fun ω ↦ f 1 * ∏ s, g s (X s ω)) ω +
      f 0 * ∏ s, g s (X s ω) - A.indicator (fun ω ↦ f 0 * ∏ s, g s (X s ω)) ω := by
    classical
    rw [Set.indicator_apply]
    split_ifs <;> simp_all
  have h2 ω : f (A.indicator 1 ω) =
      A.indicator (fun _ ↦ f 1) ω + Aᶜ.indicator (fun _ ↦ f 0) ω := by
    classical
    rw [Set.indicator_apply]
    split_ifs <;> simp_all
  have hg {c : ℝ} : Integrable (fun ω ↦ c * ∏ s, g s (X s ω)) P := by
    refine Integrable.of_bound ?_ (‖c‖ * ∏ s, ‖g s‖) (ae_of_all _ fun ω ↦ ?_)
    · exact (Finset.aestronglyMeasurable_fun_prod _ fun s _ ↦
        (g s).continuous.aestronglyMeasurable.comp_aemeasurable (mX s)).const_mul _
    · rw [norm_mul, norm_prod]
      gcongr with s
      exact (g s).norm_coe_le_norm _
  simp_rw [Pi.mul_apply, Finset.prod_apply, Function.comp_apply, h1, h2]
  rw [integral_sub, integral_add, integral_indicator₀ mA, integral_indicator₀ mA,
    integral_const_mul, integral_const_mul, integral_const_mul, integral_add,
    integral_indicator₀ mA, integral_indicator₀ mA.compl, integral_const, integral_const, h]
  · simp [measureReal_compl₀ mA]
    ring
  · exact (integrable_const _).indicator₀ mA
  · exact (integrable_const _).indicator₀ mA.compl
  · exact hg.indicator₀ mA
  · exact hg
  · exact (hg.indicator₀ mA).add hg
  · exact hg.indicator₀ mA

/-- The indicator of a set $A$ and a family of random variables $(X_1, ..., X_p)$ are independent
if for all real bounded continuous function $f$,
$$P[\mathbb{I}_A f(X_1, ..., X_p)] = P(A) P[f(X_1, ..., X_p)].$$ -/
lemma indicator_indepFun_pi_of_bcf
    {A : Set Ω} (mA : NullMeasurableSet A P) (mX : ∀ s, AEMeasurable (X s) P)
    (h : ∀ f : (Π s, E s) →ᵇ ℝ, ∫ ω in A, f (X · ω) ∂P = P.real A * ∫ ω, f (X · ω) ∂P) :
    (A.indicator (1 : Ω → ℝ)) ⟂ᵢ[P] (fun ω s ↦ X s ω) := by
  refine indicator_indepFun_pi_of_prod_bcf mA mX fun f ↦ ?_
  convert h (∏ s, (f s).compContinuous ⟨Function.eval s, by fun_prop⟩) <;> simp

/-- The indicator of a set $A$ and a random variable $X$ are independent
if for all real bounded continuous function $f$,
$$P[\mathbb{I}_A f(X)] = P(A) P[f(X)].$$ -/
lemma indicator_indepFun_of_bcf
    {A : Set Ω} (mA : NullMeasurableSet A P) (mZ : AEMeasurable Z P)
    (h : ∀ f : G →ᵇ ℝ, ∫ ω in A, f (Z ω) ∂P = P.real A * ∫ ω, f (Z ω) ∂P) :
    (A.indicator (1 : Ω → ℝ)) ⟂ᵢ[P] Z := by
  suffices (A.indicator (1 : Ω → ℝ)) ⟂ᵢ[P] (fun ω (_ : Unit) ↦ Z ω) from
    this.comp (measurable_id) (measurable_pi_apply ())
  refine indicator_indepFun_pi_of_prod_bcf mA (fun _ ↦ mZ) fun f ↦ ?_
  convert h (f ()) <;> simp

end Indicator

section IndepSets

lemma indepSets_comap_pi_of_prod_bcf
    {𝒜 : Set (Set Ω)} (m𝒜 : ∀ A ∈ 𝒜, NullMeasurableSet A P) (mX : ∀ s, AEMeasurable (X s) P)
    (h : ∀ A ∈ 𝒜, ∀ f : (s : S) → E s →ᵇ ℝ, ∫ ω in A, ∏ s, f s (X s ω) ∂P =
      P.real A * ∫ ω, ∏ s, f s (X s ω) ∂P) :
    IndepSets 𝒜 {A | MeasurableSet[MeasurableSpace.pi.comap (fun ω s ↦ X s ω)] A} P :=
  indepSets_iff_singleton_indepSets.2 fun A hA ↦ IndepFun.singleton_indepSets_of_indicator
    (indicator_indepFun_pi_of_prod_bcf (m𝒜 A hA) mX (h A hA))

lemma indepSets_comap_pi_of_bcf
    {𝒜 : Set (Set Ω)} (m𝒜 : ∀ A ∈ 𝒜, NullMeasurableSet A P) (mX : ∀ s, AEMeasurable (X s) P)
    (h : ∀ A ∈ 𝒜, ∀ f : (Π s, E s) →ᵇ ℝ, ∫ ω in A, f (X · ω) ∂P = P.real A * ∫ ω, f (X · ω) ∂P) :
    IndepSets 𝒜 {A | MeasurableSet[MeasurableSpace.pi.comap (fun ω s ↦ X s ω)] A} P :=
  indepSets_iff_singleton_indepSets.2 fun A hA ↦ IndepFun.singleton_indepSets_of_indicator
    (indicator_indepFun_pi_of_bcf (m𝒜 A hA) mX (h A hA))

lemma indepSets_comap_of_bcf
    {𝒜 : Set (Set Ω)} (m𝒜 : ∀ A ∈ 𝒜, NullMeasurableSet A P) (mZ : AEMeasurable Z P)
    (h : ∀ A ∈ 𝒜, ∀ f : G →ᵇ ℝ, ∫ ω in A, f (Z ω) ∂P = P.real A * ∫ ω, f (Z ω) ∂P) :
    IndepSets 𝒜 {A | MeasurableSet[MeasurableSpace.comap Z inferInstance] A} P :=
  indepSets_iff_singleton_indepSets.2 fun A hA ↦ IndepFun.singleton_indepSets_of_indicator
    (indicator_indepFun_of_bcf (m𝒜 A hA) mZ (h A hA))

end IndepSets

section Indep

lemma indep_comap_pi_of_prod_bcf (hm : m ≤ mΩ) (mX : ∀ s, AEMeasurable (X s) P)
    (h : ∀ A, MeasurableSet[m] A → ∀ f : (s : S) → E s →ᵇ ℝ,
      ∫ ω in A, ∏ s, f s (X s ω) ∂P = P.real A * ∫ ω, ∏ s, f s (X s ω) ∂P) :
    Indep m (MeasurableSpace.pi.comap (fun ω s ↦ X s ω)) P :=
  (Indep_iff_IndepSets _ _ P).2
    (indepSets_comap_pi_of_prod_bcf (fun A hA ↦ (hm A hA).nullMeasurableSet) mX h)

/-- A sigma-algebra $\mathcal{A}$ and a family of random variables $(X_1, ..., X_p)$ are independent
if for all set $A \in \mathcal{A}$ and for all real bounded continuous function $f$,
$$P[\mathbb{I}_A f(X_1, ..., X_p)] = P(A) P[f(X_1, ..., X_p)].$$ -/
lemma indep_comap_pi_of_bcf (hm : m ≤ mΩ) (mX : ∀ s, AEMeasurable (X s) P)
    (h : ∀ A, MeasurableSet[m] A → ∀ f : (Π s, E s) →ᵇ ℝ,
      ∫ ω in A, f (X · ω) ∂P = P.real A * ∫ ω, f (X · ω) ∂P) :
    Indep m (MeasurableSpace.pi.comap (fun ω s ↦ X s ω)) P :=
  (Indep_iff_IndepSets _ _ P).2
    (indepSets_comap_pi_of_bcf (fun A hA ↦ (hm A hA).nullMeasurableSet) mX h)

/-- A sigma-algebra $\mathcal{A}$ and a random variable $X$ are independent
if for all set $A \in \mathcal{A}$ and for all real bounded continuous function $f$,
$$P[\mathbb{I}_A f(X)] = P(A) P[f(X)].$$ -/
lemma indep_comap_of_bcf (hm : m ≤ mΩ) (mZ : AEMeasurable Z P)
    (h : ∀ A, MeasurableSet[m] A → ∀ f : G →ᵇ ℝ,
      ∫ ω in A, f (Z ω) ∂P = P.real A * ∫ ω, f (Z ω) ∂P) :
    Indep m (MeasurableSpace.comap Z inferInstance) P :=
  (Indep_iff_IndepSets _ _ P).2
    (indepSets_comap_of_bcf (fun A hA ↦ (hm A hA).nullMeasurableSet) mZ h)

end Indep

end Fintype

section Process

section IndepFun

variable [IsZeroOrProbabilityMeasure P]

lemma process_indepFun_process_of_prod_bcf
    (mX : ∀ s, Measurable (X s)) (mY : ∀ t, Measurable (Y t))
    (h : ∀ (I : Finset S) (J : Finset T) (f : (s : I) → E s →ᵇ ℝ) (g : (t : J) → F t →ᵇ ℝ),
      P[(∏ s, f s ∘ (X s)) * (∏ t, g t ∘ (Y t))] = P[∏ s, f s ∘ (X s)] * P[∏ t, g t ∘ (Y t)]) :
    IndepFun (fun ω s ↦ X s ω) (fun ω t ↦ Y t ω) P :=
  IndepFun.process_indepFun_process mX mY
    fun I J ↦ pi_indepFun_pi_of_prod_bcf (by fun_prop) (by fun_prop) (h I J)

/-- Two stochastic processes $(X_s)_{s \in S}$ and $(Y_t)_{t \in T}$ are independent if
for all $s_1, ..., s_p \in S, t_1, ..., t_q \in T$ and
for all real bounded continuous functions $f$ and $g$,
$$P[f(X_{s_1}, ..., X_{s_p}) g(Y_{t_1}, ..., Y_{t_q})] =
P[f(X_{s_1}, ..., X_{s_p})] * P[g(Y_{t_1}, ..., Y_{t_q})].$$ -/
lemma process_indepFun_process_of_bcf
    (mX : ∀ s, Measurable (X s)) (mY : ∀ t, Measurable (Y t))
    (h : ∀ (I : Finset S) (J : Finset T) (f : (Π s : I, E s) →ᵇ ℝ) (g : (Π t : J, F t) →ᵇ ℝ),
      P[fun ω ↦ f (X · ω) * g (Y · ω)] = P[fun ω ↦ f (X · ω)] * P[fun ω ↦ g (Y · ω)]) :
    IndepFun (fun ω s ↦ X s ω) (fun ω t ↦ Y t ω) P :=
  IndepFun.process_indepFun_process mX mY
    fun I J ↦ pi_indepFun_pi_of_bcf (by fun_prop) (by fun_prop) (h I J)

lemma indepFun_process_of_prod_bcf
    (mZ : AEMeasurable Z P) (mY : ∀ t, Measurable (Y t))
    (h : ∀ (f : G →ᵇ ℝ) (J : Finset T) (g : (t : J) → F t →ᵇ ℝ),
      P[f ∘ Z * (∏ t, g t ∘ (Y t))] = P[f ∘ Z] * P[∏ t, g t ∘ (Y t)]) :
    IndepFun Z (fun ω t ↦ Y t ω) P :=
  IndepFun.indepFun_process mZ mY fun J ↦
    indepFun_pi_of_prod_bcf (by fun_prop) (by fun_prop) (h · J)

lemma indepFun_process_of_bcf
    (mZ : AEMeasurable Z P) (mY : ∀ t, Measurable (Y t))
    (h : ∀ (f : G →ᵇ ℝ) (J : Finset T) (g : (Π t : J, F t) →ᵇ ℝ),
      P[fun ω ↦ f (Z ω) * g (Y · ω)] = P[f ∘ Z] * P[fun ω ↦ g (Y · ω)]) :
    IndepFun Z (fun ω t ↦ Y t ω) P :=
  IndepFun.indepFun_process mZ mY fun J ↦ indepFun_pi_of_bcf (by fun_prop) (by fun_prop) (h · J)

lemma process_indepFun_of_prod_bcf
    (mX : ∀ s, Measurable (X s)) (mU : AEMeasurable U P)
    (h : ∀ (I : Finset S) (f : (s : I) → E s →ᵇ ℝ) (g : H →ᵇ ℝ),
      P[(∏ s, f s ∘ (X s)) * g ∘ U] = P[∏ s, f s ∘ (X s)] * P[g ∘ U]) :
    IndepFun (fun ω s ↦ X s ω) U P :=
  IndepFun.process_indepFun mX mU fun I ↦ pi_indepFun_of_prod_bcf (by fun_prop) (by fun_prop) (h I)

lemma process_indepFun_of_bcf
    (mX : ∀ s, Measurable (X s)) (mU : AEMeasurable U P)
    (h : ∀ (I : Finset S) (f : (Π s : I, E s) →ᵇ ℝ) (g : H →ᵇ ℝ),
      P[fun ω ↦ f (X · ω) * g (U ω)] = P[fun ω ↦ f (X · ω)] * P[g ∘ U]) :
    IndepFun (fun ω s ↦ X s ω) U P :=
  IndepFun.process_indepFun mX mU fun I ↦ pi_indepFun_of_bcf (by fun_prop) (by fun_prop) (h I)

end IndepFun

variable [IsProbabilityMeasure P]

section Indicator

lemma indicator_indepFun_process_of_prod_bcf
    {A : Set Ω} (mA : NullMeasurableSet A P) (mX : ∀ s, Measurable (X s))
    (h : ∀ (I : Finset S) (f : (s : I) → E s →ᵇ ℝ),
      ∫ ω in A, ∏ s, f s (X s ω) ∂P = P.real A * ∫ ω, ∏ s, f s (X s ω) ∂P) :
    IndepFun (A.indicator (1 : Ω → ℝ)) (fun ω s ↦ X s ω) P :=
  IndepFun.indepFun_process ((aemeasurable_indicator_const_iff 1).2 mA) mX
    fun I ↦ indicator_indepFun_pi_of_prod_bcf mA (by fun_prop) (h I)

/-- The indicator of a set $A$ and a stochastic process $(X_s)_{s \in S}$ are independent if
for all $s_1, ..., s_p \in S$ and for all real bounded continuous function $f$,
$$P[\mathbb{I}_A f(X_{s_1}, ..., X_{s_p})] =
P(A) P[f(X_{s_1}, ..., X_{s_p})].$$ -/
lemma indicator_indepFun_process_of_bcf
    {A : Set Ω} (mA : NullMeasurableSet A P) (mX : ∀ s, Measurable (X s))
    (h : ∀ (I : Finset S) (f : (Π s : I, E s) →ᵇ ℝ),
      ∫ ω in A, f (X · ω) ∂P = P.real A * ∫ ω, f (X · ω) ∂P) :
    IndepFun (A.indicator (1 : Ω → ℝ)) (fun ω s ↦ X s ω) P :=
  IndepFun.indepFun_process ((aemeasurable_indicator_const_iff 1).2 mA) mX
    fun I ↦ indicator_indepFun_pi_of_bcf mA (by fun_prop) (h I)

end Indicator

section IndepSets

lemma indepSets_comap_process_of_prod_bcf
    {𝒜 : Set (Set Ω)} (m𝒜 : ∀ A ∈ 𝒜, NullMeasurableSet A P) (mX : ∀ s, Measurable (X s))
    (h : ∀ A ∈ 𝒜, ∀ (I : Finset S) (f : (s : I) → E s →ᵇ ℝ),
      ∫ ω in A, ∏ s, f s (X s ω) ∂P = P.real A * ∫ ω, ∏ s, f s (X s ω) ∂P) :
    IndepSets 𝒜 {A | MeasurableSet[MeasurableSpace.pi.comap (fun ω s ↦ X s ω)] A} P :=
  indepSets_iff_singleton_indepSets.2 fun A hA ↦ IndepFun.singleton_indepSets_of_indicator
    (indicator_indepFun_process_of_prod_bcf (m𝒜 A hA) mX (h A hA))

lemma indepSets_comap_process_of_bcf
    {𝒜 : Set (Set Ω)} (m𝒜 : ∀ A ∈ 𝒜, NullMeasurableSet A P) (mX : ∀ s, Measurable (X s))
    (h : ∀ A ∈ 𝒜, ∀ (I : Finset S) (f : (Π s : I, E s) →ᵇ ℝ),
      ∫ ω in A, f (X · ω) ∂P = P.real A * ∫ ω, f (X · ω) ∂P) :
    IndepSets 𝒜 {A | MeasurableSet[MeasurableSpace.pi.comap (fun ω s ↦ X s ω)] A} P :=
  indepSets_iff_singleton_indepSets.2 fun A hA ↦ IndepFun.singleton_indepSets_of_indicator
    (indicator_indepFun_process_of_bcf (m𝒜 A hA) mX (h A hA))

end IndepSets

section Indep

lemma indep_comap_process_of_prod_bcf
    (hm : m ≤ mΩ) (mX : ∀ s, Measurable (X s))
    (h : ∀ A, MeasurableSet[m] A → ∀ (I : Finset S) (f : (s : I) → E s →ᵇ ℝ),
      ∫ ω in A, ∏ s, f s (X s ω) ∂P = P.real A * ∫ ω, ∏ s, f s (X s ω) ∂P) :
    Indep m (MeasurableSpace.pi.comap (fun ω s ↦ X s ω)) P :=
  (Indep_iff_IndepSets _ _ P).2
    (indepSets_comap_process_of_prod_bcf (fun A hA ↦ (hm A hA).nullMeasurableSet) mX h)

/-- A sigma-algebra $\mathcal{A}$ and a stochastic process $(X_s)_{s \in S}$ are independent if
for all $A \in \mathcal{A}$, for all $s_1, ..., s_p \in S$ and
for all real bounded continuous function $f$,
$$P[\mathbb{I}_A f(X_{s_1}, ..., X_{s_p})] =
P(A) P[f(X_{s_1}, ..., X_{s_p})].$$ -/
lemma indep_comap_process_of_bcf
    (hm : m ≤ mΩ) (mX : ∀ s, Measurable (X s))
    (h : ∀ A, MeasurableSet[m] A → ∀ (I : Finset S) (f : (Π s : I, E s) →ᵇ ℝ),
      ∫ ω in A, f (X · ω) ∂P = P.real A * ∫ ω, f (X · ω) ∂P) :
    Indep m (MeasurableSpace.pi.comap (fun ω s ↦ X s ω)) P :=
  (Indep_iff_IndepSets _ _ P).2
    (indepSets_comap_process_of_bcf (fun A hA ↦ (hm A hA).nullMeasurableSet) mX h)

end Indep

end Process
